#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"

int foo(int a, int b) {

	if(klee_change(0,1)){
		int c=a+b;
	    return c+3;
	}
	else{
		const int d=3;
	    int c=b+a;
	    return c+d;
	}
}

int main(int argc, char *argv[]) {
  return foo(5,900);
}
